w:World.
FairFifo
 (i:Id, b, a:.
 (ab
 ( (t:. at  t<b  isnull(a(i;t)))
 ( (x.s(i;a).x) = (x.s(i;b).x)  x:Idvartype(i;x)) 

latex

Definitions	, t  T, x:AB(x), AB, a<b, b, P  Q, x:A. B(x), Id, vartype(i;x), s = t, FairFifo, World, {x:A| B(x) }, ij, Void, False, A, #$n, -n, n+m, n-m, , s(i;t).x, x.A(x), {T}, SQType(T), a(i;t), isnull(a), <a,b>, s ~ t, left+right, P  Q, Dec(P), Prop, A & B, P & Q, x:AB(x)
Lemmas	w-vartype wf, decidable lt, assert wf, w-isnull wf, w-a wf, le wf, nat sq, w-s wf, ge wf, nat properties, world wf, fair-fifo wf, Id wf, nat wf